\begin{tabbing}
$\forall$${\it the\_es}$:ES, $e$, ${\it e'}$:E.
\\[0ex]($e$ $<$ ${\it e'}$)
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((($\neg$($\uparrow$first(${\it e'}$))) c$\wedge$ (($e$ $<$ pred(${\it e'}$)) $\vee$ ($e$ = pred(${\it e'}$))))\+
\\[0ex]$\vee$ (($\uparrow$isrcv(${\it e'}$)) c$\wedge$ (($e$ $<$ sender(${\it e'}$)) $\vee$ ($e$ = sender(${\it e'}$)))))
\-
\end{tabbing}